Inference at * 
Iof proof for Lemma bool-to-dcdr wf:


  A:Type, f:(A), x:A. {f}(x)  Dec(f(x) = tt) 

latex

 by Auto 

latex

 1: 

 1: 1. A : Type
 1: 2. f : A
 1: 3. x : A
 1:   {f}(x)  Dec(f(x) = tt)
 .

Definitions

Type, x:AB(x), x:A. B(x), Dec(P), s = t, , t  T, f(a), {f}